Example 24 in [ Lucas - IC'06]

Summary: Ex24_Luc06

• TPDB format
• OBJ format
• Negative results:
  1. Lucas'
  2. Ferreira and Ribeiro's transformation
  3. Giesl and Middeldorp's transformation
  4. Zantema's transformation
• Positive results:
  1. CSDP

Ex24_Luc06 in TPDB format ( Ex24_Luc06.trs):

(VAR X)
(STRATEGY CONTEXTSENSITIVE 
  (f 2)
  (b)
  (c)
)
(RULES 
f(b,X,c) -> f(X,c,X)
c -> b
)

The CS-TRS in OBJ format (file Ex24_Luc06.obj):

			
obj Ex24_Luc06 is
  sort S .
  op f : S S S -> S [strat (2 0)] .
  op b : -> S .
  op c : -> S .
  vars X : S .
  eq f(b,X,c) = f(X,c,X) .
  eq c = b .
endo

Negative results

1. The µ-termination of Ex24_Luc06 cannot be proved by using Lucas' transformation. The TRS Ex24_Luc06_L:

   					
   	f(X) -> f(c)
   	c -> b
   	
   

   is not terminating (AProVE).
   
2. The µ-termination of Ex24_Luc06 cannot be proved by using Ferreira and Ribeiro's or Zantema's transformation .The transformed TRS Ex24_Luc06:

   						
   	f(n__b,X,n__c) -> f(X,c,X)
   	c -> b
   	b -> n__b
   	c -> n__c
   	activate(n__b) -> b
   	activate(n__c) -> c
   	activate(X) -> X
   
   

   is not terminating (AProVE).
   
3. The µ-termination of Ex24_Luc06 cannot be proved by using Giesl and Middeldorp's transformation. The TRS Ex24_Luc06_GM:

   					
   	a__f(b,X,c) -> a__f(X,a__c,X)
   	a__c -> b
   	mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
   	mark(c) -> a__c
   	mark(b) -> b
   	a__f(X1,X2,X3) -> f(X1,X2,X3)
   	a__c -> c
   
   
   

   is not terminating (AProVE).

Positive results

1. The µ-termination of Ex24_Luc06 can be proved by using CSDPs (computed by MuTerm).